YES 1.147 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((genericReplicate :: Int  ->  a  ->  [a]) :: Int  ->  a  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  genericReplicate :: Integral a => a  ->  b  ->  [b]
genericReplicate n x genericTake n (repeat x)

  genericTake :: Integral a => a  ->  [b ->  [b]
genericTake 0 _ []
genericTake [] []
genericTake n (x : xs
 | n > 0 = 
x : genericTake (n - 1) xs
genericTake _ _ error []


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((genericReplicate :: Int  ->  a  ->  [a]) :: Int  ->  a  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  genericReplicate :: Integral a => a  ->  b  ->  [b]
genericReplicate n x genericTake n (repeat x)

  genericTake :: Integral b => b  ->  [a ->  [a]
genericTake vw []
genericTake vx [] []
genericTake n (x : xs
 | n > 0 = 
x : genericTake (n - 1) xs
genericTake vy vz error []


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
genericTake vw = []
genericTake vx [] = []
genericTake n (x : xs)
 | n > 0
 = x : genericTake (n - 1) xs
genericTake vy vz = error []

is transformed to
genericTake zu vw = genericTake5 zu vw
genericTake vx [] = genericTake3 vx []
genericTake n (x : xs) = genericTake2 n (x : xs)
genericTake vy vz = genericTake0 vy vz

genericTake0 vy vz = error []

genericTake1 n x xs True = x : genericTake (n - 1) xs
genericTake1 n x xs False = genericTake0 n (x : xs)

genericTake2 n (x : xs) = genericTake1 n x xs (n > 0)
genericTake2 yv yw = genericTake0 yv yw

genericTake3 vx [] = []
genericTake3 yy yz = genericTake2 yy yz

genericTake4 True zu vw = []
genericTake4 zv zw zx = genericTake3 zw zx

genericTake5 zu vw = genericTake4 (zu == 0) zu vw
genericTake5 zy zz = genericTake3 zy zz

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ LetRed

mainModule List
  ((genericReplicate :: Int  ->  a  ->  [a]) :: Int  ->  a  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  genericReplicate :: Integral b => b  ->  a  ->  [a]
genericReplicate n x genericTake n (repeat x)

  genericTake :: Integral a => a  ->  [b ->  [b]
genericTake zu vw genericTake5 zu vw
genericTake vx [] genericTake3 vx []
genericTake n (x : xsgenericTake2 n (x : xs)
genericTake vy vz genericTake0 vy vz

  
genericTake0 vy vz error []

  
genericTake1 n x xs True x : genericTake (n - 1) xs
genericTake1 n x xs False genericTake0 n (x : xs)

  
genericTake2 n (x : xsgenericTake1 n x xs (n > 0)
genericTake2 yv yw genericTake0 yv yw

  
genericTake3 vx [] []
genericTake3 yy yz genericTake2 yy yz

  
genericTake4 True zu vw []
genericTake4 zv zw zx genericTake3 zw zx

  
genericTake5 zu vw genericTake4 (zu == 0) zu vw
genericTake5 zy zz genericTake3 zy zz


module Maybe where
  import qualified List
import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
xs
where 
xs  = x : xs

are unpacked to the following functions on top level
repeatXs vuu = vuu : repeatXs vuu



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
HASKELL
              ↳ NumRed

mainModule List
  ((genericReplicate :: Int  ->  a  ->  [a]) :: Int  ->  a  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  genericReplicate :: Integral b => b  ->  a  ->  [a]
genericReplicate n x genericTake n (repeat x)

  genericTake :: Integral b => b  ->  [a ->  [a]
genericTake zu vw genericTake5 zu vw
genericTake vx [] genericTake3 vx []
genericTake n (x : xsgenericTake2 n (x : xs)
genericTake vy vz genericTake0 vy vz

  
genericTake0 vy vz error []

  
genericTake1 n x xs True x : genericTake (n - 1) xs
genericTake1 n x xs False genericTake0 n (x : xs)

  
genericTake2 n (x : xsgenericTake1 n x xs (n > 0)
genericTake2 yv yw genericTake0 yv yw

  
genericTake3 vx [] []
genericTake3 yy yz genericTake2 yy yz

  
genericTake4 True zu vw []
genericTake4 zv zw zx genericTake3 zw zx

  
genericTake5 zu vw genericTake4 (zu == 0) zu vw
genericTake5 zy zz genericTake3 zy zz


module Maybe where
  import qualified List
import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ NumRed
HASKELL
                  ↳ Narrow

mainModule List
  (genericReplicate :: Int  ->  a  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  genericReplicate :: Integral b => b  ->  a  ->  [a]
genericReplicate n x genericTake n (repeat x)

  genericTake :: Integral b => b  ->  [a ->  [a]
genericTake zu vw genericTake5 zu vw
genericTake vx [] genericTake3 vx []
genericTake n (x : xsgenericTake2 n (x : xs)
genericTake vy vz genericTake0 vy vz

  
genericTake0 vy vz error []

  
genericTake1 n x xs True x : genericTake (n - fromInt (Pos (Succ Zero))) xs
genericTake1 n x xs False genericTake0 n (x : xs)

  
genericTake2 n (x : xsgenericTake1 n x xs (n > fromInt (Pos Zero))
genericTake2 yv yw genericTake0 yv yw

  
genericTake3 vx [] []
genericTake3 yy yz genericTake2 yy yz

  
genericTake4 True zu vw []
genericTake4 zv zw zx genericTake3 zw zx

  
genericTake5 zu vw genericTake4 (zu == fromInt (Pos Zero)) zu vw
genericTake5 zy zz genericTake3 zy zz


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ NumRed
                ↳ HASKELL
                  ↳ Narrow
QDP
                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_genericTake3(Succ(vuv3000), vuv4, ba) → new_genericTake3(vuv3000, vuv4, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: